Addressed term rewriting systems: application to a typed object calculus
Identifieur interne : 005290 ( Main/Exploration ); précédent : 005289; suivant : 005291Addressed term rewriting systems: application to a typed object calculus
Auteurs : Daniel J. Dougherty [États-Unis] ; Pierre Lescanne [France] ; Luigi LiquoriSource :
- Mathematical Structures in Computer Science [ 0960-1295 ] ; 2006-08.
Abstract
We present a formalism called addressed term rewriting systems, which can be used to model implementations of theorem proving, symbolic computation and programming languages, especially aspects of sharing, recursive computations and cyclic data structures. Addressed Term Rewriting Systems are therefore well suited to describing object-based languages, and as an example we present a language called $\lambda{\cal O}bj^{a}$, incorporating both functional and object-based features. As a case study in how reasoning about languages is supported in the ATRS formalism, we define a type system for $\lambda{\cal O}bj^{a}$ and prove a type soundness result.
Url:
DOI: 10.1017/S096012950600541X
Affiliations:
- France, États-Unis
- Auvergne-Rhône-Alpes, Massachusetts, Rhône-Alpes
- Lyon, Lyon 07
- École normale supérieure de Lyon
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002727
- to stream Istex, to step Curation: 002694
- to stream Istex, to step Checkpoint: 001138
- to stream Main, to step Merge: 005436
- to stream Main, to step Curation: 005290
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Addressed term rewriting systems: application to a typed object calculus</title><author><name sortKey="Dougherty, Daniel J" sort="Dougherty, Daniel J" uniqKey="Dougherty D" first="Daniel J." last="Dougherty">Daniel J. Dougherty</name></author><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation><country>France</country><placeName><settlement type="city">Lyon</settlement><region type="region" nuts="2">Rhône-Alpes</region></placeName><orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName></affiliation></author><author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:A5E8DB455B3FF4F827436C30D78D7BFE3EEF2CBB</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1017/S096012950600541X</idno><idno type="url">https://api.istex.fr/ark:/67375/6GQ-95JKZRX9-6/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002727</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002727</idno><idno type="wicri:Area/Istex/Curation">002694</idno><idno type="wicri:Area/Istex/Checkpoint">001138</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001138</idno><idno type="wicri:doubleKey">0960-1295:2006:Dougherty D:addressed:term:rewriting</idno><idno type="wicri:Area/Main/Merge">005436</idno><idno type="wicri:Area/Main/Curation">005290</idno><idno type="wicri:Area/Main/Exploration">005290</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">Addressed term rewriting systems: application to a typed object calculus</title><author><name sortKey="Dougherty, Daniel J" sort="Dougherty, Daniel J" uniqKey="Dougherty D" first="Daniel J." last="Dougherty">Daniel J. Dougherty</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><placeName><region type="state">Massachusetts</region></placeName><wicri:cityArea>Department of Computer Science, Worcester Polytechnic Institute, Worcester</wicri:cityArea></affiliation></author><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Laboratoire de l'Informatique du Parallélisme, École Normale Supérieure de Lyon, 46, Allée d'Italie, 69364 Lyon 07</wicri:regionArea><placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region><settlement type="city">Lyon 07</settlement></placeName><placeName><settlement type="city">Lyon</settlement><region type="region" nuts="2">Rhône-Alpes</region></placeName><orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName></affiliation></author><author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name><affiliation><wicri:noCountry code="no comma">INRIA Sophia Antipolis FR-06902 France</wicri:noCountry></affiliation></author></analytic><monogr></monogr><series><title level="j">Mathematical Structures in Computer Science</title><idno type="ISSN">0960-1295</idno><idno type="eISSN">1469-8072</idno><imprint><publisher>Cambridge University Press</publisher><pubPlace>Cambridge, UK</pubPlace><date type="published" when="2006-08">2006-08</date><biblScope unit="volume">16</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="667">667</biblScope><biblScope unit="page" to="709">709</biblScope></imprint><idno type="ISSN">0960-1295</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0960-1295</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract">We present a formalism called addressed term rewriting systems, which can be used to model implementations of theorem proving, symbolic computation and programming languages, especially aspects of sharing, recursive computations and cyclic data structures. Addressed Term Rewriting Systems are therefore well suited to describing object-based languages, and as an example we present a language called $\lambda{\cal O}bj^{a}$, incorporating both functional and object-based features. As a case study in how reasoning about languages is supported in the ATRS formalism, we define a type system for $\lambda{\cal O}bj^{a}$ and prove a type soundness result.</div></front></TEI><affiliations><list><country><li>France</li><li>États-Unis</li></country><region><li>Auvergne-Rhône-Alpes</li><li>Massachusetts</li><li>Rhône-Alpes</li></region><settlement><li>Lyon</li><li>Lyon 07</li></settlement><orgName><li>École normale supérieure de Lyon</li></orgName></list><tree><noCountry><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name></noCountry><country name="États-Unis"><region name="Massachusetts"><name sortKey="Dougherty, Daniel J" sort="Dougherty, Daniel J" uniqKey="Dougherty D" first="Daniel J." last="Dougherty">Daniel J. Dougherty</name></region></country><country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005290 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005290 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:A5E8DB455B3FF4F827436C30D78D7BFE3EEF2CBB
|texte= Addressed term rewriting systems: application to a typed object calculus
}}
| This area was generated with Dilib version V0.6.33. |  |